DLIST.DFT[VLI,LSP] - www.SailDart.org

perm filename DLIST.DFT[VLI,LSP] blob sn#381976 filedate 1978-09-08 generic text, type C, neo UTF8

COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002
C00004 ENDMK
C⊗;

newparent  `PROPT` ;;

newparent  `EQUT` ;;

newparent  `FIXT` ;;

newtypes [ ``dlist = . + dpair`` ;
           ``dpair = d # dlist`` ] ;;

newconstant ( `HD` , ":dlist->d" ) ;;

newconstant ( `TL` , ":dlist->dlist" ) ;;

newconstant ( `CONS` , ":d->(dlist->dlist)" ) ;;

newconstant ( `NIL` , ":dlist" ) ;;

newconstant ( `dummy` , ":d" ) ;;

newconstant ( `LIST` , ":d->dlist" ) ;;

NEWAXIOMS();;

AXHD  "HD == \dl:dlist.FST(OUTR dl :dpair) :d"

AXTL  "TL == \dl:dlist.SND(OUTR dl :dpair) :dlist"

AXNIL  "NIL == INL () :dlist"

AXCONS  "CONS == \d:d.\dl:dlist.INR(d,dl) :dlist"

AXNIL2  "EQ NIL NIL == TT"

AXLIST  "LIST == \d:d.INR(d, NIL) :dlist"

NNCNS1  "!d:d. !s:dlist. EQ s NIL == FF IMP EQ(CONS d s) NIL == FF"

NNCNS2  "!d:d. !s:dlist. EQ s NIL == TT IMP EQ(CONS d s)NIL == FF"

% the last two should actually be proved as facts by contradiction %